Nuprl Lemma : tree_wf
4,23
postcript
pdf
E
:Type. Tree(
E
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
Tree(
E
)
,
t
T
,
tree_con(
E
;
T
)
origin
E:Type. Tree(E) 
Type E:Type. Tree(E) Type x:A. B(x) T